abstract sig Num { sudoku : Num one -> one Num } 

abstract sig B1, B2, B3 extends Num {}

one sig N1, N2, N3 extends B1 {}
one sig N4, N5, N6 extends B2 {}
one sig N7, N8, N9 extends B3 {}
 
fact columns_onto { all y: Num | Num in sudoku[Num,y] }
fact rows_onto    { all x: Num | Num in sudoku[x,Num] }

fact B1B1_onto { Num in sudoku[B1,B1] } 
fact B1B2_onto { Num in sudoku[B1,B2] }  
fact B1B3_onto { Num in sudoku[B1,B3] } 
fact B2B1_onto { Num in sudoku[B2,B1] } 
fact B2B2_onto { Num in sudoku[B2,B2] } 
fact B2B3_onto { Num in sudoku[B2,B3] } 
fact B3B1_onto { Num in sudoku[B3,B1] } 
fact B3B2_onto { Num in sudoku[B3,B2] } 
fact B3B3_onto { Num in sudoku[B3,B3] } 

fact R1_onto {
  Num in (sudoku[N2,N2] + sudoku[N3,N2] + sudoku[N4,N2] +
          sudoku[N2,N3] + sudoku[N3,N3] + sudoku[N4,N3] +
          sudoku[N2,N4] + sudoku[N3,N4] + sudoku[N4,N4])
}
fact R2_onto {
  Num in (sudoku[N6,N2] + sudoku[N7,N2] + sudoku[N8,N2] +
          sudoku[N6,N3] + sudoku[N7,N3] + sudoku[N8,N3] +
          sudoku[N6,N4] + sudoku[N7,N4] + sudoku[N8,N4])
}
fact R3_onto {
  Num in (sudoku[N2,N6] + sudoku[N3,N6] + sudoku[N4,N6] +
          sudoku[N2,N7] + sudoku[N3,N7] + sudoku[N4,N7] +
          sudoku[N2,N8] + sudoku[N3,N8] + sudoku[N4,N8])
}
fact R4_onto {
  Num in (sudoku[N6,N6] + sudoku[N7,N6] + sudoku[N8,N6] +
          sudoku[N6,N7] + sudoku[N7,N7] + sudoku[N8,N7] +
          sudoku[N6,N8] + sudoku[N7,N8] + sudoku[N8,N8])
}

/*
This is the original example, but we've replaced it with the
Ritmeester example from the assignment.

fact problem { 
  N1->N5 + N2->N3 + N5->N7          in sudoku[N1]
  N1->N6 + N4->N1 + N5->N9 + N6->N5 in sudoku[N2]
  N2->N9 + N3->N8 + N8->N6          in sudoku[N3]
  N1->N8 + N5->N6 + N9->N3          in sudoku[N4]
  N1->N4 + N4->N8 + N6->N3 + N9->N1 in sudoku[N5]
  N1->N7 + N5->N2 + N9->N6          in sudoku[N6]
  N2->N6 + N7->N2 + N8->N8          in sudoku[N7]
  N4->N4 + N5->N1 + N6->N9 + N9->N5 in sudoku[N8]
  N5->N8 + N8->N7 + N9->N9          in sudoku[N9]
}*/

fact ritmeesterExample {
  N4->N3                            in sudoku[N1]
  N4->N7 + N7->N3                   in sudoku[N2]
  N1->N2 + N9->N8                   in sudoku[N3]
  N3->N6 + N6->N5                   in sudoku[N4]
  N2->N9 + N3->N1 + N4->N6          in sudoku[N5]
  N1->N3 + N5->N7 + N6->N1 + N7->N2 in sudoku[N6]
  N8->N3 + N9->N1                   in sudoku[N7]
  N2->N8 + N5->N4                   in sudoku[N8]
  N3->N2                            in sudoku[N9]
}

pred assertRitmeester {

}

run assertRitmeester

// Indication of time spent: 5.5 man hours
